Nuprl Lemma : outr_wf
11,40
postcript
pdf
A
,
B
:Type,
x
:(
A
+
B
). (
(
isl(
x
)))
(outr(
x
)
B
)
latex
Definitions
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
outr(
x
)
,
if
b
then
t
else
f
fi
,
ff
,
tt
,
isl(
x
)
,
b
,
b
,
False
,
prop{i:l}
Lemmas
isl
wf
,
bnot
wf
,
assert
wf
origin
A,B:Type, x:(A + B). (
(
isl(x))) 
(outr(x) 
B) A,B:Type, x:(A + B). ((isl(x))) (outr(x) B) T Qx:A. B(x)bb